

\section{Introduction}

\begin{comment}
The last decade has experienced growing interest in the verification of imperative and object oriented programs\cite{SpecSharp,Cracatoa,vcc,smallfoot}, with industry committing significant resources to software verification\cite{Hypervisor}. These approaches expect the behaviour of each function to be specified through a contract. The tools usually encode the function body in first order logic, and check that it satisfies the encoded contract. For this they often employ SMT solvers, such as Z3\cite{z3}.


% SD does not think we need the rest
% i.e. asking them to prove that
%the conjunction of the encoding program with the negation of the property is unsatisfiable.  

  
However, proving algebraic properties of functions, rather than contracts,
requires proof steps such as induction or case-splitting.
 % to handle their case-analysis based control flow. These techniques are well established and many automated theorem provers with induction and case-splitting already exist which can prove functional program properties, such as IsaPlanner\cite{isaplanner} and $\lambda$-CLAM\cite{lambdaclam}. The problem these systems face is that techniques such as induction can be applied many ways to even the most simple of properties which very quickly leads to an unmanageable search space. A tool must be able to apply these techniques generally enough so as to discover as many proofs as possible, but not suffer from this combinatorial explosion.
SMT solvers are less capable of handling such proofs, e.g., Z3 was unable to prove that \li{x + 0 = x} for the standard definition of Peano number addition (also given in \fig{exdefs}).

\end{comment}

Proving properties of functional programs requires very different techniques to those of imperative program verification. SMT solving is such a technique and is unable to prove very simple algebraic properties of recursive functions e.g., \li{x + 0 = x} for the standard definition of Peano number addition (also given in \fig{exdefs}).

Verifying functional programs has been attempted through function contracts; 
%``Extended Static Checking for Haskell''
e.g. ESC/Haskell\cite{danaesch}  
%e.g., the Extended Haskell Checker \cite{danaesch} 
proves  contracts attached to Haskell code.
These contracts are expressed through a refinement type for the function\cite{hinze06typedcontracts}. The tool implements a sound and complete projection of these type contracts into the functional program itself, whereby any execution path that violates the contract is replaced with the symbol \li{BAD}. Proving  adherence to contracts amounts  to proving  these paths to be unreachable, or removing them by simplification; such simplification steps can be done through supercompilation\cite{bolingbroke10supercompilation}. Other refinement type based verification approaches have also been tried with reasonable results\cite{refinement1,refinement2}.


\begin{figure}
\small
\begin{align*}
& Prog & ::= & \quad (TypeDef\ |\ FunType\ |\ FunDef)^* \\
\\
& FunDef & ::= & \quad \lim{f}\ \lim{x}^*\ \lim{=}\ Expr \\
& \tau & ::= & \quad \lim{x} \quad | \quad \lim{f} \quad | \quad \lim{K} \quad | \quad \lim{(}\tau_1\ \tau_2\lim{)} \\
& Expr & ::= & \quad \tau \quad | \quad \lim{case}\ \tau\ \lim{of \{}\ Alt\ (\lim{;}\ Alt)^*\ \lim{\}} \\
& Alt & ::= & \quad \lim{K}\ \lim{x}^*\ \lim{->}\ Expr \\
\\
& \type & ::= & \quad \lim{T} \quad | \quad \lim{(}\type_1\ \lim{->}\ \type_2\lim{)} \\
& TypeDef & ::= & \quad \lim{data}\ \lim{T}\ \lim{=}\ \lim{K}\ \type^*\ (\lim{|}\ \lim{K}\ \type^*)^* \\
& FunType & ::= & \quad \lim{f ::}\ \type
\end{align*}
\caption{Our functional language \textbf{HC}}
\label{fig:hcdef}
\end{figure}

However, proving algebraic properties of functions, rather than contracts,
requires proof steps such as induction or case-splitting. Tools already exist which can prove such properties using these methods\cite{clam,acl2,acl2s,isaplanner}. ACL2 is an industry strength proof system with a powerful automated prover, which uses untyped first-order Common LISP as its input language. More recently this was extended to ACL2s, the ``Sedan Edition'', with the aim of simplifying its usage and adding more powerful automated techniques. IsaPlanner is a generic proof-planning framework for the Isabelle\cite{isabelle} proof system. Its main proof tactic is a Rippling\cite{rippling} based inductive theorem prover and is what we will be referring to when we speak of IsaPlanner's theorem proving capacity. It features an ML style input language and, unlike ACL2, allows for higher-order functions and user-defined recursive data-types.

Generating induction schemes and choosing case-split steps represent a huge search space. Methods used by some tools are recursion-analysis\cite{acl2} (ACL2(s)), and ripple-analysis\cite{ripple-analysis} (CLAM and IsaPlanner). These pre-generate their induction scheme by analysing function definitions, though IsaPlanner will also backtrack on a failed proof to amend its scheme. Here we propose an alternative whereby the induction scheme is gradually built up through multiple separate proof steps. We choose these steps such that function definitions can be applied later on and introduce a concept called a \emph{critical term} to support this. The critical term is the result of symbolically executing a term within your goal property; it is either a variable which appears in the original term (signalling that one should apply induction on this variable), or a new term which was not part of the original term (signalling that one should apply a case-split on this new term). We developed Zeno, a tool based on these methods, and were very pleased to find that it could compete well with existing tools.

Zeno is fully automated and relies only on function definitions, requiring no extra lemmas to be input by the user to complete its proofs. It works by using one of ten different steps to break the proof of a property down into the proof of zero or more sub-properties, iterating until every branch of this tree has no more sub-properties left and the proof is finished. Zeno supports {\bf HC}, a minimal functional language, and {\bf PHC}, a small language of properties which allows for algebraic properties and entailment\footnote{Thus, {\bf PHC} does not support negated equality or existential or deep universal quantifiers.}.


%but all, with the exception of IsaPlanner, do not support higher-order functions and pattern matching on user defined data types, instead using destructor-style function definitions as in the LISP language, with case-splitting only on if-statements. IsaPlanner supports the Isabelle/HOL\cite{isabelle-hol} PolyML syntax which uses a mix of constructor and destructor style, featuring pattern matching alongside rewrite rules and if-statements. Zeno however uses only constructor style pattern matching and only user defined data types; rewrite rules and if-statements both become pattern matching where the latter is a match over the two cases of the boolean enumerated type. This is a feature of the Haskell language and the Glorious Glasgow Haskell Compiler\cite{ghc} in particular and we feel it adds robustness over IsaPlanner by removing alternate representations of the same function. 



%One tool for verifying properties of functional programs with these methods is ACL2\cite{acl2}. Using a first-order untyped dialect of Common LISP, ACL2 allows the construction of user guided proofs for FOL properties and features a powerful automated inductive theorem prover. More recently this tool has been extended to ACL2s, the ``ACL2 Sedan''\cite{acl2s}, with the aim of simplifying its usage and adding some more powerful automated techniques.

%The problem when automating this proof search is that steps like induction and case-splitting may be applicable in many parts of the search, and for many different subterms within a given term, thus giving rise to search space explosion. A prevalent heuristic to deal with this space explosion is rippling\cite{rippling}. Rippling dramatically trims the search space for the application of background lemmas, by giving preference to proof steps (such as the application of lemmas) which lead   towards applying the inductive step. Rippling has been successfully applied  in several tools, most particularly IsaPlanner\cite{isaplanner}, a \emph{proof planner} for the proof assistant Isabelle/HOL\cite{isabelle,isabellehol}. Notably, IsaPlanner can discover auxiliary lemmas needed for a larger proof by appealing to \emph{proof critics} when a proof search is unable to progress.
 
%In this paper we propose an alternative heuristic: rather than guide the application of lemmas and other proof steps towards making it possible to apply the inductive hypothesis, we guide the application of case-splitting, inductive steps and generalization towards making it possible to apply the function definitions. We developed Zeno, a tool based on this idea, and were very pleased to find that Zeno could compete well with both IsaPlanner and ACL2s.



% Will: removed as ACL2s does indeed support these
% many interesting properties can be expressed in {\bf PHC}, and to our knowledge, comparable automated tools do not support these quantifiers either}.


%In order to support our heuristic for reducing the search space, we have developed a concept we call a \emph{critical term}. The critical term is the result of symbolically executing a term within your goal property; it is either a variable which appears in the original term (signalling that one should apply induction on this variable), or a new term which was not part of the original term (signalling that one should apply case-splitting on this new term).

We evaluated Zeno against the tools IsaPlanner and ACL2s. Using a test suite from the IsaPlanner website we found that Zeno could prove strictly more properties than either, and with similar computation times.

This paper is organised as follows. In Section \ref{sec:language} we define {\bf HC} and {\bf PHC}. In Section \ref{sec:proof} we explain Zeno's proof output  with reference to an example. In Section \ref{sec:steps} we explain each of the steps that Zeno can take to construct a proof. In Section \ref{sec:searchspace} we describe  our heuristic for the selection of steps, and define critical terms.  In Section \ref{sec:comparison} we present a comparison between Zeno, IsaPlanner and ACL2s.
% In Section \ref{sec:related} we discuss work related to ours.
In Section \ref{sec:future} we discuss future work and we conclude in Section \ref{sec:conclusions}.

One can try Zeno online at \url{http://www.doc.ic.ac.uk/~ws506/tryzeno}, and the sources are available from \url{http://code.google.com/p/zeno}.

